How to realize LSE narrowing
Identifieur interne : 00CD21 ( Main/Exploration ); précédent : 00CD20; suivant : 00CD22How to realize LSE narrowing
Auteurs : Andreas Werner [Allemagne] ; Alexander Bockmayr [Allemagne] ; Stefan Krischer [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In [BKW93], we introduced the LSE narrowing strategy which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for arbitrary systems. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be checked for reducibility. In this paper, we first show that many of these subterms are identical. Then we describe how using left-to-right basic occurrences the number of subterms that have to be tested can be reduced drastically. Finally, based on these theoretical results, we develop an efficient implementation of LSE narrowing.
Url:
DOI: 10.1007/3-540-58431-5_7
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002755
- to stream Istex, to step Curation: 002722
- to stream Istex, to step Checkpoint: 002D10
- to stream Main, to step Merge: 00D589
- to stream Main, to step Curation: 00CD21
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">How to realize LSE narrowing</title><author><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name></author><author><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name></author><author><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:A76506DA2EBC37EFD03149360559CD4BFF96A742</idno><date when="1994" year="1994">1994</date><idno type="doi">10.1007/3-540-58431-5_7</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-9SRBS7N2-T/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002755</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002755</idno><idno type="wicri:Area/Istex/Curation">002722</idno><idno type="wicri:Area/Istex/Checkpoint">002D10</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002D10</idno><idno type="wicri:doubleKey">0302-9743:1994:Werner A:how:to:realize</idno><idno type="wicri:Area/Main/Merge">00D589</idno><idno type="wicri:Area/Main/Curation">00CD21</idno><idno type="wicri:Area/Main/Exploration">00CD21</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">How to realize LSE narrowing</title><author><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name><affiliation wicri:level="3"><country>Allemagne</country><placeName><settlement type="city">Karlsruhe</settlement><region type="land" nuts="1">Bade-Wurtemberg</region><region type="district" nuts="2">District de Karlsruhe</region></placeName><wicri:orgArea>SFB 314, Univ. Karlsruhe, D-76128</wicri:orgArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name><affiliation wicri:level="3"><country>Allemagne</country><placeName><settlement type="city">Sarrebruck</settlement><region type="land" nuts="1">Sarre (Land)</region></placeName><wicri:orgArea>MPI Informatik, Im Stadtwald, D-66123</wicri:orgArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name><affiliation></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Narrowing is a complete unification procedure for equational theories defined by canonical term rewriting systems. It is also the operational semantics of various logic and functional programming languages. In [BKW93], we introduced the LSE narrowing strategy which is complete for arbitrary canonical rewriting systems and optimal in the sense that two different LSE narrowing derivations cannot generate the same narrowing substitution. LSE narrowing improves all previously known strategies for arbitrary systems. According to their definition, LSE narrowing steps seem to be very expensive, because a large number of subterms has to be checked for reducibility. In this paper, we first show that many of these subterms are identical. Then we describe how using left-to-right basic occurrences the number of subterms that have to be tested can be reduced drastically. Finally, based on these theoretical results, we develop an efficient implementation of LSE narrowing.</div></front></TEI><affiliations><list><country><li>Allemagne</li><li>France</li></country><region><li>Bade-Wurtemberg</li><li>District de Karlsruhe</li><li>Sarre (Land)</li></region><settlement><li>Karlsruhe</li><li>Sarrebruck</li></settlement></list><tree><country name="Allemagne"><region name="Bade-Wurtemberg"><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name></region><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name><name sortKey="Bockmayr, Alexander" sort="Bockmayr, Alexander" uniqKey="Bockmayr A" first="Alexander" last="Bockmayr">Alexander Bockmayr</name><name sortKey="Werner, Andreas" sort="Werner, Andreas" uniqKey="Werner A" first="Andreas" last="Werner">Andreas Werner</name></country><country name="France"><noRegion><name sortKey="Krischer, Stefan" sort="Krischer, Stefan" uniqKey="Krischer S" first="Stefan" last="Krischer">Stefan Krischer</name></noRegion></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00CD21 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00CD21 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:A76506DA2EBC37EFD03149360559CD4BFF96A742
|texte= How to realize LSE narrowing
}}
| This area was generated with Dilib version V0.6.33. |  |